STM: chain config wf

ABS: cchead()

STM: cchead wf

ABS: cctail()

STM: cctail wf

ABS: ccpred(id)

STM: ccpred wf

ABS: ccsucc(id;num)

STM: ccsucc wf

ABS: chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num))

STM: chain config ind wf

STM: chain config-induction

ABS: chain config ind cchead compseq tag def

ABS: chain config ind cctail compseq tag def

ABS: chain config ind ccpred compseq tag def

ABS: chain config ind ccsucc compseq tag def

ABS: cchead?(x)

STM: cchead? wf

ABS: cctail?(x)

STM: cctail? wf

ABS: ccpred?(x)

STM: ccpred? wf

ABS: ccpred-id(x)

STM: ccpred-id wf

ABS: ccsucc?(x)

STM: ccsucc? wf

ABS: ccsucc-id(x)

STM: ccsucc-id wf

ABS: ccsucc-num(x)

STM: ccsucc-num wf